es:ES, T:Type, l1, l2:IdLnk, tg, a:Id, ds1, ds2:x:Id fp Type, P:(State(ds1)Prop),
Q:(State(ds2)Prop), f:(State(ds1)T).
weak-precond-send-p(es;T;;l1;tg;a;ds1;s,m. P(s,m) & (n:. n<m  P(s,n));f)
 weak-precond-send-p(es;;;l2;tg;a;ds2;s,m. Q(s,m) & (n:. n<m  Q(s,n));s,m. m)
 destination(l1) = source(l2)  Id
 destination(l2) = source(l1)  Id
 (s:State(ds1), k:. Dec(P(s,k)))
 (s:State(ds2), k:. Dec(Q(s,k)))
 (k:. @source(l1) stable s.P(s,k)  )
 (k:. @source(l2) stable s.Q(s,k)  )
 e@source(l2). kind(e) = locl(a)  Knd  Q(state after e,val(e))
 (k:. e@source(l1). P(state after e,k)  e'@destination(l1).Q(state after e',k))
 (e:E. kind(e) = rcv(l2,tg)  Knd  (k:. k<val(e)  P(state after e,k)))
 (k:, e:E.
 (kind(e) = rcv(l1,tg)  Knd  val(e) = f((state when sender(e)),k)  Q(state after e,k))
 e@destination(l1).True
 (k:. e@destination(l1).Q(state after e,k)) 

latex

Definitions	e@i.P(e), t  T, P  Q, A, ij, AB, False, Prop, x:A. B(x), A & B, P & Q, x:A. B(x), x(s1,s2), , SQType(T), {T}, x. t(x), State(ds), state@i, T, True, P  Q, Dec(P), x(s)
Lemmas	nat properties, ge wf, nat wf, es-loc wf, es-E wf, le wf, es-le-total, decidable lt, stable-implies2, subtype rel dep function, es-vartype wf, fpf-cap wf, id-deq wf, top wf, subtype rel self, Id sq, es-state-after wf, es-sender wf, es-kind-rcv, stable-implies4, es-le-loc, lsrc wf, ldst wf, es-loc-rcv